YES(O(1),O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { #equal(@x, @y) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , -(@x, @y) -> #sub(@x, @y) , div(@x, @y) -> #div(@x, @y) , eratos(@l) -> eratos#1(@l) , eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs))) , eratos#1(nil()) -> nil() , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' } Weak Trs: { #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() , #natsub(@x, #0()) -> @x , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We add following dependency tuples: Strict DPs: { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , *^#(@x, @y) -> c_2(#mult^#(@x, @y)) , -^#(@x, @y) -> c_3(#sub^#(@x, @y)) , div^#(@x, @y) -> c_4(#div^#(@x, @y)) , eratos^#(@l) -> c_5(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , eratos#1^#(nil()) -> c_7() , filter^#(@p, @l) -> c_8(filter#1^#(@l, @p)) , filter#1^#(::(@x, @xs), @p) -> c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) , filter#1^#(nil(), @p) -> c_10() , filter#2^#(@xs', @p, @x) -> c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), #equal^#(mod(@x, @p), #0()), mod^#(@x, @p)) , filter#3^#(#false(), @x, @xs') -> c_13() , filter#3^#(#true(), @x, @xs') -> c_14() , mod^#(@x, @y) -> c_12(-^#(@x, *(@y, div(@x, @y))), *^#(@y, div(@x, @y)), div^#(@x, @y)) } Weak DPs: { #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_16() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_17() , #eq^#(nil(), nil()) -> c_18() , #eq^#(#0(), #0()) -> c_19() , #eq^#(#0(), #s(@y)) -> c_20() , #eq^#(#0(), #neg(@y)) -> c_21() , #eq^#(#0(), #pos(@y)) -> c_22() , #eq^#(#s(@x), #0()) -> c_23() , #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y)) , #eq^#(#neg(@x), #0()) -> c_25() , #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_27() , #eq^#(#pos(@x), #0()) -> c_28() , #eq^#(#pos(@x), #neg(@y)) -> c_29() , #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y)) , #mult^#(#0(), #0()) -> c_31() , #mult^#(#0(), #neg(@y)) -> c_32() , #mult^#(#0(), #pos(@y)) -> c_33() , #mult^#(#neg(@x), #0()) -> c_34() , #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y)) , #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #0()) -> c_37() , #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y)) , #sub^#(@x, #0()) -> c_40() , #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y))) , #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y))) , #div^#(#0(), #0()) -> c_43() , #div^#(#0(), #neg(@y)) -> c_44() , #div^#(#0(), #pos(@y)) -> c_45() , #div^#(#neg(@x), #0()) -> c_46() , #div^#(#neg(@x), #neg(@y)) -> c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#neg(@x), #pos(@y)) -> c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #0()) -> c_49() , #div^#(#pos(@x), #neg(@y)) -> c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #pos(@y)) -> c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #and^#(#false(), #false()) -> c_65() , #and^#(#false(), #true()) -> c_66() , #and^#(#true(), #false()) -> c_67() , #and^#(#true(), #true()) -> c_68() , #natmult^#(#0(), @y) -> c_85() , #natmult^#(#s(@x), @y) -> c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , #add^#(#0(), @y) -> c_52() , #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #positive^#(#0()) -> c_73() , #positive^#(#s(@x)) -> c_74() , #positive^#(#neg(@x)) -> c_75() , #positive^#(#pos(@x)) -> c_76() , #natdiv^#(#0(), #0()) -> c_69() , #natdiv^#(#0(), #s(@y)) -> c_70() , #natdiv^#(#s(@x), #0()) -> c_71() , #natdiv^#(#s(@x), #s(@y)) -> c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y)) , #negative^#(#0()) -> c_77() , #negative^#(#s(@x)) -> c_78() , #negative^#(#neg(@x)) -> c_79() , #negative^#(#pos(@x)) -> c_80() , #pred^#(#0()) -> c_57() , #pred^#(#neg(#s(@x))) -> c_58() , #pred^#(#pos(#s(#0()))) -> c_59() , #pred^#(#pos(#s(#s(@x)))) -> c_60() , #succ^#(#0()) -> c_61() , #succ^#(#neg(#s(#0()))) -> c_62() , #succ^#(#neg(#s(#s(@x)))) -> c_63() , #succ^#(#pos(#s(@x))) -> c_64() , #natdiv'^#(#0(), @y) -> c_89() , #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y)) , #natdiv'^#(#underflow(), @y) -> c_91() , #divsub^#(#0(), #0()) -> c_81() , #divsub^#(#0(), #s(@y)) -> c_82() , #divsub^#(#s(@x), #0()) -> c_83() , #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y)) , #natadd^#(#0(), @y) -> c_87() , #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y)) , #natsub^#(@x, #0()) -> c_92() , #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , *^#(@x, @y) -> c_2(#mult^#(@x, @y)) , -^#(@x, @y) -> c_3(#sub^#(@x, @y)) , div^#(@x, @y) -> c_4(#div^#(@x, @y)) , eratos^#(@l) -> c_5(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , eratos#1^#(nil()) -> c_7() , filter^#(@p, @l) -> c_8(filter#1^#(@l, @p)) , filter#1^#(::(@x, @xs), @p) -> c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) , filter#1^#(nil(), @p) -> c_10() , filter#2^#(@xs', @p, @x) -> c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), #equal^#(mod(@x, @p), #0()), mod^#(@x, @p)) , filter#3^#(#false(), @x, @xs') -> c_13() , filter#3^#(#true(), @x, @xs') -> c_14() , mod^#(@x, @y) -> c_12(-^#(@x, *(@y, div(@x, @y))), *^#(@y, div(@x, @y)), div^#(@x, @y)) } Weak DPs: { #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_16() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_17() , #eq^#(nil(), nil()) -> c_18() , #eq^#(#0(), #0()) -> c_19() , #eq^#(#0(), #s(@y)) -> c_20() , #eq^#(#0(), #neg(@y)) -> c_21() , #eq^#(#0(), #pos(@y)) -> c_22() , #eq^#(#s(@x), #0()) -> c_23() , #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y)) , #eq^#(#neg(@x), #0()) -> c_25() , #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_27() , #eq^#(#pos(@x), #0()) -> c_28() , #eq^#(#pos(@x), #neg(@y)) -> c_29() , #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y)) , #mult^#(#0(), #0()) -> c_31() , #mult^#(#0(), #neg(@y)) -> c_32() , #mult^#(#0(), #pos(@y)) -> c_33() , #mult^#(#neg(@x), #0()) -> c_34() , #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y)) , #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #0()) -> c_37() , #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y)) , #sub^#(@x, #0()) -> c_40() , #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y))) , #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y))) , #div^#(#0(), #0()) -> c_43() , #div^#(#0(), #neg(@y)) -> c_44() , #div^#(#0(), #pos(@y)) -> c_45() , #div^#(#neg(@x), #0()) -> c_46() , #div^#(#neg(@x), #neg(@y)) -> c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#neg(@x), #pos(@y)) -> c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #0()) -> c_49() , #div^#(#pos(@x), #neg(@y)) -> c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #pos(@y)) -> c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #and^#(#false(), #false()) -> c_65() , #and^#(#false(), #true()) -> c_66() , #and^#(#true(), #false()) -> c_67() , #and^#(#true(), #true()) -> c_68() , #natmult^#(#0(), @y) -> c_85() , #natmult^#(#s(@x), @y) -> c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , #add^#(#0(), @y) -> c_52() , #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #positive^#(#0()) -> c_73() , #positive^#(#s(@x)) -> c_74() , #positive^#(#neg(@x)) -> c_75() , #positive^#(#pos(@x)) -> c_76() , #natdiv^#(#0(), #0()) -> c_69() , #natdiv^#(#0(), #s(@y)) -> c_70() , #natdiv^#(#s(@x), #0()) -> c_71() , #natdiv^#(#s(@x), #s(@y)) -> c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y)) , #negative^#(#0()) -> c_77() , #negative^#(#s(@x)) -> c_78() , #negative^#(#neg(@x)) -> c_79() , #negative^#(#pos(@x)) -> c_80() , #pred^#(#0()) -> c_57() , #pred^#(#neg(#s(@x))) -> c_58() , #pred^#(#pos(#s(#0()))) -> c_59() , #pred^#(#pos(#s(#s(@x)))) -> c_60() , #succ^#(#0()) -> c_61() , #succ^#(#neg(#s(#0()))) -> c_62() , #succ^#(#neg(#s(#s(@x)))) -> c_63() , #succ^#(#pos(#s(@x))) -> c_64() , #natdiv'^#(#0(), @y) -> c_89() , #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y)) , #natdiv'^#(#underflow(), @y) -> c_91() , #divsub^#(#0(), #0()) -> c_81() , #divsub^#(#0(), #s(@y)) -> c_82() , #divsub^#(#s(@x), #0()) -> c_83() , #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y)) , #natadd^#(#0(), @y) -> c_87() , #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y)) , #natsub^#(@x, #0()) -> c_92() , #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , eratos(@l) -> eratos#1(@l) , eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs))) , eratos#1(nil()) -> nil() , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() , #natsub(@x, #0()) -> @x , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We estimate the number of application of {1,2,3,4,7,10,12,13} by applications of Pre({1,2,3,4,7,10,12,13}) = {5,8,11,14}. Here rules are labeled as follows: DPs: { 1: #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , 2: *^#(@x, @y) -> c_2(#mult^#(@x, @y)) , 3: -^#(@x, @y) -> c_3(#sub^#(@x, @y)) , 4: div^#(@x, @y) -> c_4(#div^#(@x, @y)) , 5: eratos^#(@l) -> c_5(eratos#1^#(@l)) , 6: eratos#1^#(::(@x, @xs)) -> c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , 7: eratos#1^#(nil()) -> c_7() , 8: filter^#(@p, @l) -> c_8(filter#1^#(@l, @p)) , 9: filter#1^#(::(@x, @xs), @p) -> c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) , 10: filter#1^#(nil(), @p) -> c_10() , 11: filter#2^#(@xs', @p, @x) -> c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), #equal^#(mod(@x, @p), #0()), mod^#(@x, @p)) , 12: filter#3^#(#false(), @x, @xs') -> c_13() , 13: filter#3^#(#true(), @x, @xs') -> c_14() , 14: mod^#(@x, @y) -> c_12(-^#(@x, *(@y, div(@x, @y))), *^#(@y, div(@x, @y)), div^#(@x, @y)) , 15: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , 16: #eq^#(::(@x_1, @x_2), nil()) -> c_16() , 17: #eq^#(nil(), ::(@y_1, @y_2)) -> c_17() , 18: #eq^#(nil(), nil()) -> c_18() , 19: #eq^#(#0(), #0()) -> c_19() , 20: #eq^#(#0(), #s(@y)) -> c_20() , 21: #eq^#(#0(), #neg(@y)) -> c_21() , 22: #eq^#(#0(), #pos(@y)) -> c_22() , 23: #eq^#(#s(@x), #0()) -> c_23() , 24: #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y)) , 25: #eq^#(#neg(@x), #0()) -> c_25() , 26: #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y)) , 27: #eq^#(#neg(@x), #pos(@y)) -> c_27() , 28: #eq^#(#pos(@x), #0()) -> c_28() , 29: #eq^#(#pos(@x), #neg(@y)) -> c_29() , 30: #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y)) , 31: #mult^#(#0(), #0()) -> c_31() , 32: #mult^#(#0(), #neg(@y)) -> c_32() , 33: #mult^#(#0(), #pos(@y)) -> c_33() , 34: #mult^#(#neg(@x), #0()) -> c_34() , 35: #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y)) , 36: #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y)) , 37: #mult^#(#pos(@x), #0()) -> c_37() , 38: #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y)) , 39: #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y)) , 40: #sub^#(@x, #0()) -> c_40() , 41: #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y))) , 42: #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y))) , 43: #div^#(#0(), #0()) -> c_43() , 44: #div^#(#0(), #neg(@y)) -> c_44() , 45: #div^#(#0(), #pos(@y)) -> c_45() , 46: #div^#(#neg(@x), #0()) -> c_46() , 47: #div^#(#neg(@x), #neg(@y)) -> c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 48: #div^#(#neg(@x), #pos(@y)) -> c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 49: #div^#(#pos(@x), #0()) -> c_49() , 50: #div^#(#pos(@x), #neg(@y)) -> c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 51: #div^#(#pos(@x), #pos(@y)) -> c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 52: #and^#(#false(), #false()) -> c_65() , 53: #and^#(#false(), #true()) -> c_66() , 54: #and^#(#true(), #false()) -> c_67() , 55: #and^#(#true(), #true()) -> c_68() , 56: #natmult^#(#0(), @y) -> c_85() , 57: #natmult^#(#s(@x), @y) -> c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , 58: #add^#(#0(), @y) -> c_52() , 59: #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y)) , 60: #add^#(#neg(#s(#s(@x))), @y) -> c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 61: #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y)) , 62: #add^#(#pos(#s(#s(@x))), @y) -> c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 63: #positive^#(#0()) -> c_73() , 64: #positive^#(#s(@x)) -> c_74() , 65: #positive^#(#neg(@x)) -> c_75() , 66: #positive^#(#pos(@x)) -> c_76() , 67: #natdiv^#(#0(), #0()) -> c_69() , 68: #natdiv^#(#0(), #s(@y)) -> c_70() , 69: #natdiv^#(#s(@x), #0()) -> c_71() , 70: #natdiv^#(#s(@x), #s(@y)) -> c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y)) , 71: #negative^#(#0()) -> c_77() , 72: #negative^#(#s(@x)) -> c_78() , 73: #negative^#(#neg(@x)) -> c_79() , 74: #negative^#(#pos(@x)) -> c_80() , 75: #pred^#(#0()) -> c_57() , 76: #pred^#(#neg(#s(@x))) -> c_58() , 77: #pred^#(#pos(#s(#0()))) -> c_59() , 78: #pred^#(#pos(#s(#s(@x)))) -> c_60() , 79: #succ^#(#0()) -> c_61() , 80: #succ^#(#neg(#s(#0()))) -> c_62() , 81: #succ^#(#neg(#s(#s(@x)))) -> c_63() , 82: #succ^#(#pos(#s(@x))) -> c_64() , 83: #natdiv'^#(#0(), @y) -> c_89() , 84: #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y)) , 85: #natdiv'^#(#underflow(), @y) -> c_91() , 86: #divsub^#(#0(), #0()) -> c_81() , 87: #divsub^#(#0(), #s(@y)) -> c_82() , 88: #divsub^#(#s(@x), #0()) -> c_83() , 89: #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y)) , 90: #natadd^#(#0(), @y) -> c_87() , 91: #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y)) , 92: #natsub^#(@x, #0()) -> c_92() , 93: #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { eratos^#(@l) -> c_5(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , filter^#(@p, @l) -> c_8(filter#1^#(@l, @p)) , filter#1^#(::(@x, @xs), @p) -> c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) , filter#2^#(@xs', @p, @x) -> c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), #equal^#(mod(@x, @p), #0()), mod^#(@x, @p)) , mod^#(@x, @y) -> c_12(-^#(@x, *(@y, div(@x, @y))), *^#(@y, div(@x, @y)), div^#(@x, @y)) } Weak DPs: { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_16() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_17() , #eq^#(nil(), nil()) -> c_18() , #eq^#(#0(), #0()) -> c_19() , #eq^#(#0(), #s(@y)) -> c_20() , #eq^#(#0(), #neg(@y)) -> c_21() , #eq^#(#0(), #pos(@y)) -> c_22() , #eq^#(#s(@x), #0()) -> c_23() , #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y)) , #eq^#(#neg(@x), #0()) -> c_25() , #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_27() , #eq^#(#pos(@x), #0()) -> c_28() , #eq^#(#pos(@x), #neg(@y)) -> c_29() , #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y)) , *^#(@x, @y) -> c_2(#mult^#(@x, @y)) , #mult^#(#0(), #0()) -> c_31() , #mult^#(#0(), #neg(@y)) -> c_32() , #mult^#(#0(), #pos(@y)) -> c_33() , #mult^#(#neg(@x), #0()) -> c_34() , #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y)) , #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #0()) -> c_37() , #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y)) , -^#(@x, @y) -> c_3(#sub^#(@x, @y)) , #sub^#(@x, #0()) -> c_40() , #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y))) , #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y))) , div^#(@x, @y) -> c_4(#div^#(@x, @y)) , #div^#(#0(), #0()) -> c_43() , #div^#(#0(), #neg(@y)) -> c_44() , #div^#(#0(), #pos(@y)) -> c_45() , #div^#(#neg(@x), #0()) -> c_46() , #div^#(#neg(@x), #neg(@y)) -> c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#neg(@x), #pos(@y)) -> c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #0()) -> c_49() , #div^#(#pos(@x), #neg(@y)) -> c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #pos(@y)) -> c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , eratos#1^#(nil()) -> c_7() , filter#1^#(nil(), @p) -> c_10() , filter#3^#(#false(), @x, @xs') -> c_13() , filter#3^#(#true(), @x, @xs') -> c_14() , #and^#(#false(), #false()) -> c_65() , #and^#(#false(), #true()) -> c_66() , #and^#(#true(), #false()) -> c_67() , #and^#(#true(), #true()) -> c_68() , #natmult^#(#0(), @y) -> c_85() , #natmult^#(#s(@x), @y) -> c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , #add^#(#0(), @y) -> c_52() , #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #positive^#(#0()) -> c_73() , #positive^#(#s(@x)) -> c_74() , #positive^#(#neg(@x)) -> c_75() , #positive^#(#pos(@x)) -> c_76() , #natdiv^#(#0(), #0()) -> c_69() , #natdiv^#(#0(), #s(@y)) -> c_70() , #natdiv^#(#s(@x), #0()) -> c_71() , #natdiv^#(#s(@x), #s(@y)) -> c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y)) , #negative^#(#0()) -> c_77() , #negative^#(#s(@x)) -> c_78() , #negative^#(#neg(@x)) -> c_79() , #negative^#(#pos(@x)) -> c_80() , #pred^#(#0()) -> c_57() , #pred^#(#neg(#s(@x))) -> c_58() , #pred^#(#pos(#s(#0()))) -> c_59() , #pred^#(#pos(#s(#s(@x)))) -> c_60() , #succ^#(#0()) -> c_61() , #succ^#(#neg(#s(#0()))) -> c_62() , #succ^#(#neg(#s(#s(@x)))) -> c_63() , #succ^#(#pos(#s(@x))) -> c_64() , #natdiv'^#(#0(), @y) -> c_89() , #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y)) , #natdiv'^#(#underflow(), @y) -> c_91() , #divsub^#(#0(), #0()) -> c_81() , #divsub^#(#0(), #s(@y)) -> c_82() , #divsub^#(#s(@x), #0()) -> c_83() , #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y)) , #natadd^#(#0(), @y) -> c_87() , #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y)) , #natsub^#(@x, #0()) -> c_92() , #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , eratos(@l) -> eratos#1(@l) , eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs))) , eratos#1(nil()) -> nil() , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() , #natsub(@x, #0()) -> @x , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We estimate the number of application of {6} by applications of Pre({6}) = {5}. Here rules are labeled as follows: DPs: { 1: eratos^#(@l) -> c_5(eratos#1^#(@l)) , 2: eratos#1^#(::(@x, @xs)) -> c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , 3: filter^#(@p, @l) -> c_8(filter#1^#(@l, @p)) , 4: filter#1^#(::(@x, @xs), @p) -> c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) , 5: filter#2^#(@xs', @p, @x) -> c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), #equal^#(mod(@x, @p), #0()), mod^#(@x, @p)) , 6: mod^#(@x, @y) -> c_12(-^#(@x, *(@y, div(@x, @y))), *^#(@y, div(@x, @y)), div^#(@x, @y)) , 7: #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , 8: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , 9: #eq^#(::(@x_1, @x_2), nil()) -> c_16() , 10: #eq^#(nil(), ::(@y_1, @y_2)) -> c_17() , 11: #eq^#(nil(), nil()) -> c_18() , 12: #eq^#(#0(), #0()) -> c_19() , 13: #eq^#(#0(), #s(@y)) -> c_20() , 14: #eq^#(#0(), #neg(@y)) -> c_21() , 15: #eq^#(#0(), #pos(@y)) -> c_22() , 16: #eq^#(#s(@x), #0()) -> c_23() , 17: #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y)) , 18: #eq^#(#neg(@x), #0()) -> c_25() , 19: #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y)) , 20: #eq^#(#neg(@x), #pos(@y)) -> c_27() , 21: #eq^#(#pos(@x), #0()) -> c_28() , 22: #eq^#(#pos(@x), #neg(@y)) -> c_29() , 23: #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y)) , 24: *^#(@x, @y) -> c_2(#mult^#(@x, @y)) , 25: #mult^#(#0(), #0()) -> c_31() , 26: #mult^#(#0(), #neg(@y)) -> c_32() , 27: #mult^#(#0(), #pos(@y)) -> c_33() , 28: #mult^#(#neg(@x), #0()) -> c_34() , 29: #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y)) , 30: #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y)) , 31: #mult^#(#pos(@x), #0()) -> c_37() , 32: #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y)) , 33: #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y)) , 34: -^#(@x, @y) -> c_3(#sub^#(@x, @y)) , 35: #sub^#(@x, #0()) -> c_40() , 36: #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y))) , 37: #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y))) , 38: div^#(@x, @y) -> c_4(#div^#(@x, @y)) , 39: #div^#(#0(), #0()) -> c_43() , 40: #div^#(#0(), #neg(@y)) -> c_44() , 41: #div^#(#0(), #pos(@y)) -> c_45() , 42: #div^#(#neg(@x), #0()) -> c_46() , 43: #div^#(#neg(@x), #neg(@y)) -> c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 44: #div^#(#neg(@x), #pos(@y)) -> c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 45: #div^#(#pos(@x), #0()) -> c_49() , 46: #div^#(#pos(@x), #neg(@y)) -> c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 47: #div^#(#pos(@x), #pos(@y)) -> c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 48: eratos#1^#(nil()) -> c_7() , 49: filter#1^#(nil(), @p) -> c_10() , 50: filter#3^#(#false(), @x, @xs') -> c_13() , 51: filter#3^#(#true(), @x, @xs') -> c_14() , 52: #and^#(#false(), #false()) -> c_65() , 53: #and^#(#false(), #true()) -> c_66() , 54: #and^#(#true(), #false()) -> c_67() , 55: #and^#(#true(), #true()) -> c_68() , 56: #natmult^#(#0(), @y) -> c_85() , 57: #natmult^#(#s(@x), @y) -> c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , 58: #add^#(#0(), @y) -> c_52() , 59: #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y)) , 60: #add^#(#neg(#s(#s(@x))), @y) -> c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 61: #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y)) , 62: #add^#(#pos(#s(#s(@x))), @y) -> c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 63: #positive^#(#0()) -> c_73() , 64: #positive^#(#s(@x)) -> c_74() , 65: #positive^#(#neg(@x)) -> c_75() , 66: #positive^#(#pos(@x)) -> c_76() , 67: #natdiv^#(#0(), #0()) -> c_69() , 68: #natdiv^#(#0(), #s(@y)) -> c_70() , 69: #natdiv^#(#s(@x), #0()) -> c_71() , 70: #natdiv^#(#s(@x), #s(@y)) -> c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y)) , 71: #negative^#(#0()) -> c_77() , 72: #negative^#(#s(@x)) -> c_78() , 73: #negative^#(#neg(@x)) -> c_79() , 74: #negative^#(#pos(@x)) -> c_80() , 75: #pred^#(#0()) -> c_57() , 76: #pred^#(#neg(#s(@x))) -> c_58() , 77: #pred^#(#pos(#s(#0()))) -> c_59() , 78: #pred^#(#pos(#s(#s(@x)))) -> c_60() , 79: #succ^#(#0()) -> c_61() , 80: #succ^#(#neg(#s(#0()))) -> c_62() , 81: #succ^#(#neg(#s(#s(@x)))) -> c_63() , 82: #succ^#(#pos(#s(@x))) -> c_64() , 83: #natdiv'^#(#0(), @y) -> c_89() , 84: #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y)) , 85: #natdiv'^#(#underflow(), @y) -> c_91() , 86: #divsub^#(#0(), #0()) -> c_81() , 87: #divsub^#(#0(), #s(@y)) -> c_82() , 88: #divsub^#(#s(@x), #0()) -> c_83() , 89: #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y)) , 90: #natadd^#(#0(), @y) -> c_87() , 91: #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y)) , 92: #natsub^#(@x, #0()) -> c_92() , 93: #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { eratos^#(@l) -> c_5(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , filter^#(@p, @l) -> c_8(filter#1^#(@l, @p)) , filter#1^#(::(@x, @xs), @p) -> c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) , filter#2^#(@xs', @p, @x) -> c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), #equal^#(mod(@x, @p), #0()), mod^#(@x, @p)) } Weak DPs: { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_16() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_17() , #eq^#(nil(), nil()) -> c_18() , #eq^#(#0(), #0()) -> c_19() , #eq^#(#0(), #s(@y)) -> c_20() , #eq^#(#0(), #neg(@y)) -> c_21() , #eq^#(#0(), #pos(@y)) -> c_22() , #eq^#(#s(@x), #0()) -> c_23() , #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y)) , #eq^#(#neg(@x), #0()) -> c_25() , #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_27() , #eq^#(#pos(@x), #0()) -> c_28() , #eq^#(#pos(@x), #neg(@y)) -> c_29() , #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y)) , *^#(@x, @y) -> c_2(#mult^#(@x, @y)) , #mult^#(#0(), #0()) -> c_31() , #mult^#(#0(), #neg(@y)) -> c_32() , #mult^#(#0(), #pos(@y)) -> c_33() , #mult^#(#neg(@x), #0()) -> c_34() , #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y)) , #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #0()) -> c_37() , #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y)) , -^#(@x, @y) -> c_3(#sub^#(@x, @y)) , #sub^#(@x, #0()) -> c_40() , #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y))) , #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y))) , div^#(@x, @y) -> c_4(#div^#(@x, @y)) , #div^#(#0(), #0()) -> c_43() , #div^#(#0(), #neg(@y)) -> c_44() , #div^#(#0(), #pos(@y)) -> c_45() , #div^#(#neg(@x), #0()) -> c_46() , #div^#(#neg(@x), #neg(@y)) -> c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#neg(@x), #pos(@y)) -> c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #0()) -> c_49() , #div^#(#pos(@x), #neg(@y)) -> c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #pos(@y)) -> c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , eratos#1^#(nil()) -> c_7() , filter#1^#(nil(), @p) -> c_10() , filter#3^#(#false(), @x, @xs') -> c_13() , filter#3^#(#true(), @x, @xs') -> c_14() , mod^#(@x, @y) -> c_12(-^#(@x, *(@y, div(@x, @y))), *^#(@y, div(@x, @y)), div^#(@x, @y)) , #and^#(#false(), #false()) -> c_65() , #and^#(#false(), #true()) -> c_66() , #and^#(#true(), #false()) -> c_67() , #and^#(#true(), #true()) -> c_68() , #natmult^#(#0(), @y) -> c_85() , #natmult^#(#s(@x), @y) -> c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , #add^#(#0(), @y) -> c_52() , #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #positive^#(#0()) -> c_73() , #positive^#(#s(@x)) -> c_74() , #positive^#(#neg(@x)) -> c_75() , #positive^#(#pos(@x)) -> c_76() , #natdiv^#(#0(), #0()) -> c_69() , #natdiv^#(#0(), #s(@y)) -> c_70() , #natdiv^#(#s(@x), #0()) -> c_71() , #natdiv^#(#s(@x), #s(@y)) -> c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y)) , #negative^#(#0()) -> c_77() , #negative^#(#s(@x)) -> c_78() , #negative^#(#neg(@x)) -> c_79() , #negative^#(#pos(@x)) -> c_80() , #pred^#(#0()) -> c_57() , #pred^#(#neg(#s(@x))) -> c_58() , #pred^#(#pos(#s(#0()))) -> c_59() , #pred^#(#pos(#s(#s(@x)))) -> c_60() , #succ^#(#0()) -> c_61() , #succ^#(#neg(#s(#0()))) -> c_62() , #succ^#(#neg(#s(#s(@x)))) -> c_63() , #succ^#(#pos(#s(@x))) -> c_64() , #natdiv'^#(#0(), @y) -> c_89() , #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y)) , #natdiv'^#(#underflow(), @y) -> c_91() , #divsub^#(#0(), #0()) -> c_81() , #divsub^#(#0(), #s(@y)) -> c_82() , #divsub^#(#s(@x), #0()) -> c_83() , #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y)) , #natadd^#(#0(), @y) -> c_87() , #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y)) , #natsub^#(@x, #0()) -> c_92() , #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , eratos(@l) -> eratos#1(@l) , eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs))) , eratos#1(nil()) -> nil() , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() , #natsub(@x, #0()) -> @x , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We estimate the number of application of {5} by applications of Pre({5}) = {4}. Here rules are labeled as follows: DPs: { 1: eratos^#(@l) -> c_5(eratos#1^#(@l)) , 2: eratos#1^#(::(@x, @xs)) -> c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , 3: filter^#(@p, @l) -> c_8(filter#1^#(@l, @p)) , 4: filter#1^#(::(@x, @xs), @p) -> c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) , 5: filter#2^#(@xs', @p, @x) -> c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), #equal^#(mod(@x, @p), #0()), mod^#(@x, @p)) , 6: #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , 7: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , 8: #eq^#(::(@x_1, @x_2), nil()) -> c_16() , 9: #eq^#(nil(), ::(@y_1, @y_2)) -> c_17() , 10: #eq^#(nil(), nil()) -> c_18() , 11: #eq^#(#0(), #0()) -> c_19() , 12: #eq^#(#0(), #s(@y)) -> c_20() , 13: #eq^#(#0(), #neg(@y)) -> c_21() , 14: #eq^#(#0(), #pos(@y)) -> c_22() , 15: #eq^#(#s(@x), #0()) -> c_23() , 16: #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y)) , 17: #eq^#(#neg(@x), #0()) -> c_25() , 18: #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y)) , 19: #eq^#(#neg(@x), #pos(@y)) -> c_27() , 20: #eq^#(#pos(@x), #0()) -> c_28() , 21: #eq^#(#pos(@x), #neg(@y)) -> c_29() , 22: #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y)) , 23: *^#(@x, @y) -> c_2(#mult^#(@x, @y)) , 24: #mult^#(#0(), #0()) -> c_31() , 25: #mult^#(#0(), #neg(@y)) -> c_32() , 26: #mult^#(#0(), #pos(@y)) -> c_33() , 27: #mult^#(#neg(@x), #0()) -> c_34() , 28: #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y)) , 29: #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y)) , 30: #mult^#(#pos(@x), #0()) -> c_37() , 31: #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y)) , 32: #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y)) , 33: -^#(@x, @y) -> c_3(#sub^#(@x, @y)) , 34: #sub^#(@x, #0()) -> c_40() , 35: #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y))) , 36: #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y))) , 37: div^#(@x, @y) -> c_4(#div^#(@x, @y)) , 38: #div^#(#0(), #0()) -> c_43() , 39: #div^#(#0(), #neg(@y)) -> c_44() , 40: #div^#(#0(), #pos(@y)) -> c_45() , 41: #div^#(#neg(@x), #0()) -> c_46() , 42: #div^#(#neg(@x), #neg(@y)) -> c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 43: #div^#(#neg(@x), #pos(@y)) -> c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 44: #div^#(#pos(@x), #0()) -> c_49() , 45: #div^#(#pos(@x), #neg(@y)) -> c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 46: #div^#(#pos(@x), #pos(@y)) -> c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 47: eratos#1^#(nil()) -> c_7() , 48: filter#1^#(nil(), @p) -> c_10() , 49: filter#3^#(#false(), @x, @xs') -> c_13() , 50: filter#3^#(#true(), @x, @xs') -> c_14() , 51: mod^#(@x, @y) -> c_12(-^#(@x, *(@y, div(@x, @y))), *^#(@y, div(@x, @y)), div^#(@x, @y)) , 52: #and^#(#false(), #false()) -> c_65() , 53: #and^#(#false(), #true()) -> c_66() , 54: #and^#(#true(), #false()) -> c_67() , 55: #and^#(#true(), #true()) -> c_68() , 56: #natmult^#(#0(), @y) -> c_85() , 57: #natmult^#(#s(@x), @y) -> c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , 58: #add^#(#0(), @y) -> c_52() , 59: #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y)) , 60: #add^#(#neg(#s(#s(@x))), @y) -> c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 61: #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y)) , 62: #add^#(#pos(#s(#s(@x))), @y) -> c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 63: #positive^#(#0()) -> c_73() , 64: #positive^#(#s(@x)) -> c_74() , 65: #positive^#(#neg(@x)) -> c_75() , 66: #positive^#(#pos(@x)) -> c_76() , 67: #natdiv^#(#0(), #0()) -> c_69() , 68: #natdiv^#(#0(), #s(@y)) -> c_70() , 69: #natdiv^#(#s(@x), #0()) -> c_71() , 70: #natdiv^#(#s(@x), #s(@y)) -> c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y)) , 71: #negative^#(#0()) -> c_77() , 72: #negative^#(#s(@x)) -> c_78() , 73: #negative^#(#neg(@x)) -> c_79() , 74: #negative^#(#pos(@x)) -> c_80() , 75: #pred^#(#0()) -> c_57() , 76: #pred^#(#neg(#s(@x))) -> c_58() , 77: #pred^#(#pos(#s(#0()))) -> c_59() , 78: #pred^#(#pos(#s(#s(@x)))) -> c_60() , 79: #succ^#(#0()) -> c_61() , 80: #succ^#(#neg(#s(#0()))) -> c_62() , 81: #succ^#(#neg(#s(#s(@x)))) -> c_63() , 82: #succ^#(#pos(#s(@x))) -> c_64() , 83: #natdiv'^#(#0(), @y) -> c_89() , 84: #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y)) , 85: #natdiv'^#(#underflow(), @y) -> c_91() , 86: #divsub^#(#0(), #0()) -> c_81() , 87: #divsub^#(#0(), #s(@y)) -> c_82() , 88: #divsub^#(#s(@x), #0()) -> c_83() , 89: #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y)) , 90: #natadd^#(#0(), @y) -> c_87() , 91: #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y)) , 92: #natsub^#(@x, #0()) -> c_92() , 93: #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { eratos^#(@l) -> c_5(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , filter^#(@p, @l) -> c_8(filter#1^#(@l, @p)) , filter#1^#(::(@x, @xs), @p) -> c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) } Weak DPs: { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_16() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_17() , #eq^#(nil(), nil()) -> c_18() , #eq^#(#0(), #0()) -> c_19() , #eq^#(#0(), #s(@y)) -> c_20() , #eq^#(#0(), #neg(@y)) -> c_21() , #eq^#(#0(), #pos(@y)) -> c_22() , #eq^#(#s(@x), #0()) -> c_23() , #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y)) , #eq^#(#neg(@x), #0()) -> c_25() , #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_27() , #eq^#(#pos(@x), #0()) -> c_28() , #eq^#(#pos(@x), #neg(@y)) -> c_29() , #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y)) , *^#(@x, @y) -> c_2(#mult^#(@x, @y)) , #mult^#(#0(), #0()) -> c_31() , #mult^#(#0(), #neg(@y)) -> c_32() , #mult^#(#0(), #pos(@y)) -> c_33() , #mult^#(#neg(@x), #0()) -> c_34() , #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y)) , #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #0()) -> c_37() , #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y)) , -^#(@x, @y) -> c_3(#sub^#(@x, @y)) , #sub^#(@x, #0()) -> c_40() , #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y))) , #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y))) , div^#(@x, @y) -> c_4(#div^#(@x, @y)) , #div^#(#0(), #0()) -> c_43() , #div^#(#0(), #neg(@y)) -> c_44() , #div^#(#0(), #pos(@y)) -> c_45() , #div^#(#neg(@x), #0()) -> c_46() , #div^#(#neg(@x), #neg(@y)) -> c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#neg(@x), #pos(@y)) -> c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #0()) -> c_49() , #div^#(#pos(@x), #neg(@y)) -> c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #pos(@y)) -> c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , eratos#1^#(nil()) -> c_7() , filter#1^#(nil(), @p) -> c_10() , filter#2^#(@xs', @p, @x) -> c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), #equal^#(mod(@x, @p), #0()), mod^#(@x, @p)) , filter#3^#(#false(), @x, @xs') -> c_13() , filter#3^#(#true(), @x, @xs') -> c_14() , mod^#(@x, @y) -> c_12(-^#(@x, *(@y, div(@x, @y))), *^#(@y, div(@x, @y)), div^#(@x, @y)) , #and^#(#false(), #false()) -> c_65() , #and^#(#false(), #true()) -> c_66() , #and^#(#true(), #false()) -> c_67() , #and^#(#true(), #true()) -> c_68() , #natmult^#(#0(), @y) -> c_85() , #natmult^#(#s(@x), @y) -> c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , #add^#(#0(), @y) -> c_52() , #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #positive^#(#0()) -> c_73() , #positive^#(#s(@x)) -> c_74() , #positive^#(#neg(@x)) -> c_75() , #positive^#(#pos(@x)) -> c_76() , #natdiv^#(#0(), #0()) -> c_69() , #natdiv^#(#0(), #s(@y)) -> c_70() , #natdiv^#(#s(@x), #0()) -> c_71() , #natdiv^#(#s(@x), #s(@y)) -> c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y)) , #negative^#(#0()) -> c_77() , #negative^#(#s(@x)) -> c_78() , #negative^#(#neg(@x)) -> c_79() , #negative^#(#pos(@x)) -> c_80() , #pred^#(#0()) -> c_57() , #pred^#(#neg(#s(@x))) -> c_58() , #pred^#(#pos(#s(#0()))) -> c_59() , #pred^#(#pos(#s(#s(@x)))) -> c_60() , #succ^#(#0()) -> c_61() , #succ^#(#neg(#s(#0()))) -> c_62() , #succ^#(#neg(#s(#s(@x)))) -> c_63() , #succ^#(#pos(#s(@x))) -> c_64() , #natdiv'^#(#0(), @y) -> c_89() , #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y)) , #natdiv'^#(#underflow(), @y) -> c_91() , #divsub^#(#0(), #0()) -> c_81() , #divsub^#(#0(), #s(@y)) -> c_82() , #divsub^#(#s(@x), #0()) -> c_83() , #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y)) , #natadd^#(#0(), @y) -> c_87() , #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y)) , #natsub^#(@x, #0()) -> c_92() , #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , eratos(@l) -> eratos#1(@l) , eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs))) , eratos#1(nil()) -> nil() , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() , #natsub(@x, #0()) -> @x , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_16() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_17() , #eq^#(nil(), nil()) -> c_18() , #eq^#(#0(), #0()) -> c_19() , #eq^#(#0(), #s(@y)) -> c_20() , #eq^#(#0(), #neg(@y)) -> c_21() , #eq^#(#0(), #pos(@y)) -> c_22() , #eq^#(#s(@x), #0()) -> c_23() , #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y)) , #eq^#(#neg(@x), #0()) -> c_25() , #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_27() , #eq^#(#pos(@x), #0()) -> c_28() , #eq^#(#pos(@x), #neg(@y)) -> c_29() , #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y)) , *^#(@x, @y) -> c_2(#mult^#(@x, @y)) , #mult^#(#0(), #0()) -> c_31() , #mult^#(#0(), #neg(@y)) -> c_32() , #mult^#(#0(), #pos(@y)) -> c_33() , #mult^#(#neg(@x), #0()) -> c_34() , #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y)) , #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #0()) -> c_37() , #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y)) , -^#(@x, @y) -> c_3(#sub^#(@x, @y)) , #sub^#(@x, #0()) -> c_40() , #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y))) , #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y))) , div^#(@x, @y) -> c_4(#div^#(@x, @y)) , #div^#(#0(), #0()) -> c_43() , #div^#(#0(), #neg(@y)) -> c_44() , #div^#(#0(), #pos(@y)) -> c_45() , #div^#(#neg(@x), #0()) -> c_46() , #div^#(#neg(@x), #neg(@y)) -> c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#neg(@x), #pos(@y)) -> c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #0()) -> c_49() , #div^#(#pos(@x), #neg(@y)) -> c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #pos(@y)) -> c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , eratos#1^#(nil()) -> c_7() , filter#1^#(nil(), @p) -> c_10() , filter#2^#(@xs', @p, @x) -> c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), #equal^#(mod(@x, @p), #0()), mod^#(@x, @p)) , filter#3^#(#false(), @x, @xs') -> c_13() , filter#3^#(#true(), @x, @xs') -> c_14() , mod^#(@x, @y) -> c_12(-^#(@x, *(@y, div(@x, @y))), *^#(@y, div(@x, @y)), div^#(@x, @y)) , #and^#(#false(), #false()) -> c_65() , #and^#(#false(), #true()) -> c_66() , #and^#(#true(), #false()) -> c_67() , #and^#(#true(), #true()) -> c_68() , #natmult^#(#0(), @y) -> c_85() , #natmult^#(#s(@x), @y) -> c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , #add^#(#0(), @y) -> c_52() , #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #positive^#(#0()) -> c_73() , #positive^#(#s(@x)) -> c_74() , #positive^#(#neg(@x)) -> c_75() , #positive^#(#pos(@x)) -> c_76() , #natdiv^#(#0(), #0()) -> c_69() , #natdiv^#(#0(), #s(@y)) -> c_70() , #natdiv^#(#s(@x), #0()) -> c_71() , #natdiv^#(#s(@x), #s(@y)) -> c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y)) , #negative^#(#0()) -> c_77() , #negative^#(#s(@x)) -> c_78() , #negative^#(#neg(@x)) -> c_79() , #negative^#(#pos(@x)) -> c_80() , #pred^#(#0()) -> c_57() , #pred^#(#neg(#s(@x))) -> c_58() , #pred^#(#pos(#s(#0()))) -> c_59() , #pred^#(#pos(#s(#s(@x)))) -> c_60() , #succ^#(#0()) -> c_61() , #succ^#(#neg(#s(#0()))) -> c_62() , #succ^#(#neg(#s(#s(@x)))) -> c_63() , #succ^#(#pos(#s(@x))) -> c_64() , #natdiv'^#(#0(), @y) -> c_89() , #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y)) , #natdiv'^#(#underflow(), @y) -> c_91() , #divsub^#(#0(), #0()) -> c_81() , #divsub^#(#0(), #s(@y)) -> c_82() , #divsub^#(#s(@x), #0()) -> c_83() , #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y)) , #natadd^#(#0(), @y) -> c_87() , #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y)) , #natsub^#(@x, #0()) -> c_92() , #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { eratos^#(@l) -> c_5(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , filter^#(@p, @l) -> c_8(filter#1^#(@l, @p)) , filter#1^#(::(@x, @xs), @p) -> c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , eratos(@l) -> eratos#1(@l) , eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs))) , eratos#1(nil()) -> nil() , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() , #natsub(@x, #0()) -> @x , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { filter#1^#(::(@x, @xs), @p) -> c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { eratos^#(@l) -> c_1(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , filter^#(@p, @l) -> c_3(filter#1^#(@l, @p)) , filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , eratos(@l) -> eratos#1(@l) , eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs))) , eratos#1(nil()) -> nil() , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() , #natsub(@x, #0()) -> @x , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We replace rewrite rules by usable rules: Weak Usable Rules: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { eratos^#(@l) -> c_1(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , filter^#(@p, @l) -> c_3(filter#1^#(@l, @p)) , filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We decompose the input problem according to the dependency graph into the upper component { eratos^#(@l) -> c_1(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) } and lower component { filter^#(@p, @l) -> c_3(filter#1^#(@l, @p)) , filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) } Further, following extension rules are added to the lower component. { eratos^#(@l) -> eratos#1^#(@l) , eratos#1^#(::(@x, @xs)) -> eratos^#(filter(@x, @xs)) , eratos#1^#(::(@x, @xs)) -> filter^#(@x, @xs) } TcT solves the upper component with certificate YES(O(1),O(n^1)). Sub-proof: ---------- We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { eratos^#(@l) -> c_1(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { eratos#1^#(::(@x, @xs)) -> c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { eratos^#(@l) -> c_1(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_2(eratos^#(filter(@x, @xs))) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: eratos^#(@l) -> c_1(eratos#1^#(@l)) } Trs: { #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , filter#3(#true(), @x, @xs') -> @xs' } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [#equal](x1, x2) = [0] [#eq](x1, x2) = [0] [*](x1, x2) = [0] [#mult](x1, x2) = [0] [-](x1, x2) = [1] x1 + [0] [#sub](x1, x2) = [1] x1 + [1] [div](x1, x2) = [0] [#div](x1, x2) = [0] [::](x1, x2) = [1] x1 + [1] x2 + [1] [filter](x1, x2) = [1] x2 + [0] [nil] = [0] [filter#1](x1, x2) = [1] x1 + [0] [filter#2](x1, x2, x3) = [1] x1 + [1] x3 + [1] [mod](x1, x2) = [1] [#0] = [1] [filter#3](x1, x2, x3) = [1] x2 + [1] x3 + [1] [#false] = [0] [#true] = [1] [#add](x1, x2) = [1] x1 + [0] [#s](x1) = [0] [#neg](x1) = [0] [#pred](x1) = [0] [#pos](x1) = [0] [#succ](x1) = [0] [#and](x1, x2) = [0] [#divByZero] = [0] [#natdiv](x1, x2) = [0] [#positive](x1) = [0] [#negative](x1) = [0] [#divsub](x1, x2) = [0] [#underflow] = [0] [#natmult](x1, x2) = [0] [#natadd](x1, x2) = [0] [#natdiv'](x1, x2) = [0] [#equal^#](x1, x2) = [0] [#eq^#](x1, x2) = [0] [*^#](x1, x2) = [0] [#mult^#](x1, x2) = [0] [-^#](x1, x2) = [0] [#sub^#](x1, x2) = [0] [div^#](x1, x2) = [0] [#div^#](x1, x2) = [0] [eratos^#](x1) = [1] x1 + [1] [eratos#1^#](x1) = [1] x1 + [0] [filter^#](x1, x2) = [0] [filter#1^#](x1, x2) = [0] [filter#2^#](x1, x2, x3) = [0] [filter#3^#](x1, x2, x3) = [0] [mod^#](x1, x2) = [0] [#and^#](x1, x2) = [0] [#natmult^#](x1, x2) = [0] [#add^#](x1, x2) = [0] [#positive^#](x1) = [0] [#natdiv^#](x1, x2) = [0] [#negative^#](x1) = [0] [#pred^#](x1) = [0] [#succ^#](x1) = [0] [#natdiv'^#](x1, x2) = [0] [#divsub^#](x1, x2) = [0] [#natadd^#](x1, x2) = [0] [#natsub^#](x1, x2) = [0] [c_1](x1) = [0] [c_2](x1, x2) = [0] [c] = [0] [c_1](x1) = [1] x1 + [0] [c_2](x1) = [1] x1 + [0] This order satisfies following ordering constraints [filter(@p, @l)] = [1] @l + [0] >= [1] @l + [0] = [filter#1(@l, @p)] [filter#1(::(@x, @xs), @p)] = [1] @x + [1] @xs + [1] >= [1] @x + [1] @xs + [1] = [filter#2(filter(@p, @xs), @p, @x)] [filter#1(nil(), @p)] = [0] >= [0] = [nil()] [filter#2(@xs', @p, @x)] = [1] @x + [1] @xs' + [1] >= [1] @x + [1] @xs' + [1] = [filter#3(#equal(mod(@x, @p), #0()), @x, @xs')] [filter#3(#false(), @x, @xs')] = [1] @x + [1] @xs' + [1] >= [1] @x + [1] @xs' + [1] = [::(@x, @xs')] [filter#3(#true(), @x, @xs')] = [1] @x + [1] @xs' + [1] > [1] @xs' + [0] = [@xs'] [eratos^#(@l)] = [1] @l + [1] > [1] @l + [0] = [c_1(eratos#1^#(@l))] [eratos#1^#(::(@x, @xs))] = [1] @x + [1] @xs + [1] >= [1] @xs + [1] = [c_2(eratos^#(filter(@x, @xs)))] Consider the set of all dependency pairs DPs: { 1: eratos^#(@l) -> c_1(eratos#1^#(@l)) , 2: eratos#1^#(::(@x, @xs)) -> c_2(eratos^#(filter(@x, @xs))) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {1}. These cover all (indirect) predecessors of dependency pairs {1,2}, their number of application is equally bounded. The dependency pairs are shifted into the corresponding weak component(s). We apply the transformation 'removetails' on the sub-problem: Weak DPs: { eratos^#(@l) -> c_1(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_2(eratos^#(filter(@x, @xs))) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() } StartTerms: basic terms Strategy: innermost The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { eratos^#(@l) -> c_1(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_2(eratos^#(filter(@x, @xs))) } We apply the transformation 'usablerules' on the sub-problem: Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() } StartTerms: basic terms Strategy: innermost No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { filter^#(@p, @l) -> c_3(filter#1^#(@l, @p)) , filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) } Weak DPs: { eratos^#(@l) -> eratos#1^#(@l) , eratos#1^#(::(@x, @xs)) -> eratos^#(filter(@x, @xs)) , eratos#1^#(::(@x, @xs)) -> filter^#(@x, @xs) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 2: filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) , 4: eratos#1^#(::(@x, @xs)) -> eratos^#(filter(@x, @xs)) , 5: eratos#1^#(::(@x, @xs)) -> filter^#(@x, @xs) } Trs: { div(@x, @y) -> #div(@x, @y) , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#true(), @x, @xs') -> @xs' , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_3) = {1}, Uargs(c_4) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [#equal](x1, x2) = [1] x2 + [0] [#eq](x1, x2) = [0] [*](x1, x2) = [0] [#mult](x1, x2) = [0] [-](x1, x2) = [1] x2 + [0] [#sub](x1, x2) = [1] x1 + [0] [div](x1, x2) = [1] [#div](x1, x2) = [0] [::](x1, x2) = [1] x1 + [1] x2 + [1] [filter](x1, x2) = [1] x2 + [0] [nil] = [0] [filter#1](x1, x2) = [1] x1 + [0] [filter#2](x1, x2, x3) = [1] x1 + [1] x3 + [1] [mod](x1, x2) = [1] [#0] = [0] [filter#3](x1, x2, x3) = [1] x2 + [1] x3 + [1] [#false] = [0] [#true] = [1] [#add](x1, x2) = [1] x1 + [0] [#s](x1) = [0] [#neg](x1) = [1] x1 + [0] [#pred](x1) = [0] [#pos](x1) = [1] [#succ](x1) = [0] [#and](x1, x2) = [0] [#divByZero] = [0] [#natdiv](x1, x2) = [0] [#positive](x1) = [0] [#negative](x1) = [0] [#divsub](x1, x2) = [0] [#underflow] = [0] [#natmult](x1, x2) = [0] [#natadd](x1, x2) = [0] [#natdiv'](x1, x2) = [0] [#equal^#](x1, x2) = [0] [#eq^#](x1, x2) = [0] [*^#](x1, x2) = [0] [#mult^#](x1, x2) = [0] [-^#](x1, x2) = [0] [#sub^#](x1, x2) = [0] [div^#](x1, x2) = [0] [#div^#](x1, x2) = [0] [eratos^#](x1) = [1] x1 + [0] [eratos#1^#](x1) = [1] x1 + [0] [filter^#](x1, x2) = [1] x2 + [0] [filter#1^#](x1, x2) = [1] x1 + [0] [filter#2^#](x1, x2, x3) = [0] [filter#3^#](x1, x2, x3) = [0] [mod^#](x1, x2) = [0] [#and^#](x1, x2) = [0] [#natmult^#](x1, x2) = [0] [#add^#](x1, x2) = [0] [#positive^#](x1) = [0] [#natdiv^#](x1, x2) = [0] [#negative^#](x1) = [0] [#pred^#](x1) = [0] [#succ^#](x1) = [0] [#natdiv'^#](x1, x2) = [0] [#divsub^#](x1, x2) = [0] [#natadd^#](x1, x2) = [0] [#natsub^#](x1, x2) = [0] [c_3](x1) = [1] x1 + [0] [c_4](x1) = [1] x1 + [0] This order satisfies following ordering constraints [filter(@p, @l)] = [1] @l + [0] >= [1] @l + [0] = [filter#1(@l, @p)] [filter#1(::(@x, @xs), @p)] = [1] @x + [1] @xs + [1] >= [1] @x + [1] @xs + [1] = [filter#2(filter(@p, @xs), @p, @x)] [filter#1(nil(), @p)] = [0] >= [0] = [nil()] [filter#2(@xs', @p, @x)] = [1] @x + [1] @xs' + [1] >= [1] @x + [1] @xs' + [1] = [filter#3(#equal(mod(@x, @p), #0()), @x, @xs')] [filter#3(#false(), @x, @xs')] = [1] @x + [1] @xs' + [1] >= [1] @x + [1] @xs' + [1] = [::(@x, @xs')] [filter#3(#true(), @x, @xs')] = [1] @x + [1] @xs' + [1] > [1] @xs' + [0] = [@xs'] [eratos^#(@l)] = [1] @l + [0] >= [1] @l + [0] = [eratos#1^#(@l)] [eratos#1^#(::(@x, @xs))] = [1] @x + [1] @xs + [1] > [1] @xs + [0] = [eratos^#(filter(@x, @xs))] [eratos#1^#(::(@x, @xs))] = [1] @x + [1] @xs + [1] > [1] @xs + [0] = [filter^#(@x, @xs)] [filter^#(@p, @l)] = [1] @l + [0] >= [1] @l + [0] = [c_3(filter#1^#(@l, @p))] [filter#1^#(::(@x, @xs), @p)] = [1] @x + [1] @xs + [1] > [1] @xs + [0] = [c_4(filter^#(@p, @xs))] Consider the set of all dependency pairs DPs: { 1: filter^#(@p, @l) -> c_3(filter#1^#(@l, @p)) , 2: filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) , 3: eratos^#(@l) -> eratos#1^#(@l) , 4: eratos#1^#(::(@x, @xs)) -> eratos^#(filter(@x, @xs)) , 5: eratos#1^#(::(@x, @xs)) -> filter^#(@x, @xs) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {2,4,5}. These cover all (indirect) predecessors of dependency pairs {1,2,3,4,5}, their number of application is equally bounded. The dependency pairs are shifted into the corresponding weak component(s). We apply the transformation 'removetails' on the sub-problem: Weak DPs: { eratos^#(@l) -> eratos#1^#(@l) , eratos#1^#(::(@x, @xs)) -> eratos^#(filter(@x, @xs)) , eratos#1^#(::(@x, @xs)) -> filter^#(@x, @xs) , filter^#(@p, @l) -> c_3(filter#1^#(@l, @p)) , filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() } StartTerms: basic terms Strategy: innermost The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { eratos^#(@l) -> eratos#1^#(@l) , eratos#1^#(::(@x, @xs)) -> eratos^#(filter(@x, @xs)) , eratos#1^#(::(@x, @xs)) -> filter^#(@x, @xs) , filter^#(@p, @l) -> c_3(filter#1^#(@l, @p)) , filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) } We apply the transformation 'usablerules' on the sub-problem: Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() } StartTerms: basic terms Strategy: innermost No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Wall-time: 1.468601s CPU-time: 11.037s Wall-time: 3.015849s CPU-time: 22.525s Hurray, we answered YES(O(1),O(n^2))